H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.0420000000000003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ BR

mainModule Main

((intToDigit :: Int -> Char) :: Int -> Char)

module Main where

import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

mainModule Main

((intToDigit :: Int -> Char) :: Int -> Char)

module Main where

import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

The following Function with conditions

intToDigit i

| i >= 0 && i <= 9

= toEnum (fromEnum '0' + i)

| i >= 10 && i <= 15

= toEnum (fromEnum 'a' + i - 10)

| otherwise

= error []

is transformed to

intToDigit i = intToDigit3 i

intToDigit1 i True = toEnum (fromEnum 'a' + i - 10)

intToDigit1 i False = intToDigit0 i otherwise

intToDigit0 i True = error []

intToDigit2 i True = toEnum (fromEnum '0' + i)

intToDigit2 i False = intToDigit1 i (i >= 10 && i <= 15)

intToDigit3 i = intToDigit2 i (i >= 0 && i <= 9)

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

mainModule Main

((intToDigit :: Int -> Char) :: Int -> Char)

module Main where

import qualified Prelude

Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

mainModule Main

(intToDigit :: Int -> Char)

module Main where

import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="intToDigit",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="intToDigit vx3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="intToDigit3 vx3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5 -> 6[label="",style="dashed", color="red", weight=0];
5[label="intToDigit2 vx3 (vx3 >= Pos Zero && vx3 <= Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))",fontsize=16,color="magenta"];5 -> 7[label="",style="dashed", color="magenta", weight=3];
5 -> 8[label="",style="dashed", color="magenta", weight=3];
7[label="vx3",fontsize=16,color="green",shape="box"];8[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))",fontsize=16,color="green",shape="box"];6[label="intToDigit2 vx5 (vx5 >= Pos Zero && vx5 <= Pos (Succ vx6))",fontsize=16,color="black",shape="triangle"];6 -> 9[label="",style="solid", color="black", weight=3];
9[label="intToDigit2 vx5 (compare vx5 (Pos Zero) /= LT && vx5 <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];9 -> 10[label="",style="solid", color="black", weight=3];
10[label="intToDigit2 vx5 (not (compare vx5 (Pos Zero) == LT) && vx5 <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];10 -> 11[label="",style="solid", color="black", weight=3];
11[label="intToDigit2 vx5 (not (primCmpInt vx5 (Pos Zero) == LT) && vx5 <= Pos (Succ vx6))",fontsize=16,color="burlywood",shape="box"];1063[label="vx5/Pos vx50",fontsize=10,color="white",style="solid",shape="box"];11 -> 1063[label="",style="solid", color="burlywood", weight=9];
1063 -> 12[label="",style="solid", color="burlywood", weight=3];
1064[label="vx5/Neg vx50",fontsize=10,color="white",style="solid",shape="box"];11 -> 1064[label="",style="solid", color="burlywood", weight=9];
1064 -> 13[label="",style="solid", color="burlywood", weight=3];
12[label="intToDigit2 (Pos vx50) (not (primCmpInt (Pos vx50) (Pos Zero) == LT) && Pos vx50 <= Pos (Succ vx6))",fontsize=16,color="burlywood",shape="box"];1065[label="vx50/Succ vx500",fontsize=10,color="white",style="solid",shape="box"];12 -> 1065[label="",style="solid", color="burlywood", weight=9];
1065 -> 14[label="",style="solid", color="burlywood", weight=3];
1066[label="vx50/Zero",fontsize=10,color="white",style="solid",shape="box"];12 -> 1066[label="",style="solid", color="burlywood", weight=9];
1066 -> 15[label="",style="solid", color="burlywood", weight=3];
13[label="intToDigit2 (Neg vx50) (not (primCmpInt (Neg vx50) (Pos Zero) == LT) && Neg vx50 <= Pos (Succ vx6))",fontsize=16,color="burlywood",shape="box"];1067[label="vx50/Succ vx500",fontsize=10,color="white",style="solid",shape="box"];13 -> 1067[label="",style="solid", color="burlywood", weight=9];
1067 -> 16[label="",style="solid", color="burlywood", weight=3];
1068[label="vx50/Zero",fontsize=10,color="white",style="solid",shape="box"];13 -> 1068[label="",style="solid", color="burlywood", weight=9];
1068 -> 17[label="",style="solid", color="burlywood", weight=3];
14[label="intToDigit2 (Pos (Succ vx500)) (not (primCmpInt (Pos (Succ vx500)) (Pos Zero) == LT) && Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];14 -> 18[label="",style="solid", color="black", weight=3];
15[label="intToDigit2 (Pos Zero) (not (primCmpInt (Pos Zero) (Pos Zero) == LT) && Pos Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];15 -> 19[label="",style="solid", color="black", weight=3];
16[label="intToDigit2 (Neg (Succ vx500)) (not (primCmpInt (Neg (Succ vx500)) (Pos Zero) == LT) && Neg (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];16 -> 20[label="",style="solid", color="black", weight=3];
17[label="intToDigit2 (Neg Zero) (not (primCmpInt (Neg Zero) (Pos Zero) == LT) && Neg Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];17 -> 21[label="",style="solid", color="black", weight=3];
18[label="intToDigit2 (Pos (Succ vx500)) (not (primCmpNat (Succ vx500) Zero == LT) && Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];18 -> 22[label="",style="solid", color="black", weight=3];
19[label="intToDigit2 (Pos Zero) (not (EQ == LT) && Pos Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];19 -> 23[label="",style="solid", color="black", weight=3];
20[label="intToDigit2 (Neg (Succ vx500)) (not (LT == LT) && Neg (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="intToDigit2 (Neg Zero) (not (EQ == LT) && Neg Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="intToDigit2 (Pos (Succ vx500)) (not (GT == LT) && Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="intToDigit2 (Pos Zero) (not False && Pos Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24[label="intToDigit2 (Neg (Succ vx500)) (not True && Neg (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];24 -> 28[label="",style="solid", color="black", weight=3];
25[label="intToDigit2 (Neg Zero) (not False && Neg Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];25 -> 29[label="",style="solid", color="black", weight=3];
26[label="intToDigit2 (Pos (Succ vx500)) (not False && Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];26 -> 30[label="",style="solid", color="black", weight=3];
27[label="intToDigit2 (Pos Zero) (True && Pos Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];27 -> 31[label="",style="solid", color="black", weight=3];
28[label="intToDigit2 (Neg (Succ vx500)) (False && Neg (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];28 -> 32[label="",style="solid", color="black", weight=3];
29[label="intToDigit2 (Neg Zero) (True && Neg Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];29 -> 33[label="",style="solid", color="black", weight=3];
30[label="intToDigit2 (Pos (Succ vx500)) (True && Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];30 -> 34[label="",style="solid", color="black", weight=3];
31[label="intToDigit2 (Pos Zero) (Pos Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];31 -> 35[label="",style="solid", color="black", weight=3];
32[label="intToDigit2 (Neg (Succ vx500)) False",fontsize=16,color="black",shape="box"];32 -> 36[label="",style="solid", color="black", weight=3];
33[label="intToDigit2 (Neg Zero) (Neg Zero <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];33 -> 37[label="",style="solid", color="black", weight=3];
34[label="intToDigit2 (Pos (Succ vx500)) (Pos (Succ vx500) <= Pos (Succ vx6))",fontsize=16,color="black",shape="box"];34 -> 38[label="",style="solid", color="black", weight=3];
35[label="intToDigit2 (Pos Zero) (compare (Pos Zero) (Pos (Succ vx6)) /= GT)",fontsize=16,color="black",shape="box"];35 -> 39[label="",style="solid", color="black", weight=3];
36 -> 46[label="",style="dashed", color="red", weight=0];
36[label="intToDigit1 (Neg (Succ vx500)) (Neg (Succ vx500) >= Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))) && Neg (Succ vx500) <= Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))",fontsize=16,color="magenta"];36 -> 47[label="",style="dashed", color="magenta", weight=3];
36 -> 48[label="",style="dashed", color="magenta", weight=3];
36 -> 49[label="",style="dashed", color="magenta", weight=3];
37[label="intToDigit2 (Neg Zero) (compare (Neg Zero) (Pos (Succ vx6)) /= GT)",fontsize=16,color="black",shape="box"];37 -> 43[label="",style="solid", color="black", weight=3];
38[label="intToDigit2 (Pos (Succ vx500)) (compare (Pos (Succ vx500)) (Pos (Succ vx6)) /= GT)",fontsize=16,color="black",shape="box"];38 -> 44[label="",style="solid", color="black", weight=3];
39[label="intToDigit2 (Pos Zero) (not (compare (Pos Zero) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];39 -> 45[label="",style="solid", color="black", weight=3];
47[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))",fontsize=16,color="green",shape="box"];48[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))",fontsize=16,color="green",shape="box"];49[label="vx500",fontsize=16,color="green",shape="box"];46[label="intToDigit1 (Neg (Succ vx11)) (Neg (Succ vx11) >= Pos (Succ vx12) && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="triangle"];46 -> 53[label="",style="solid", color="black", weight=3];
43[label="intToDigit2 (Neg Zero) (not (compare (Neg Zero) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];43 -> 54[label="",style="solid", color="black", weight=3];
44[label="intToDigit2 (Pos (Succ vx500)) (not (compare (Pos (Succ vx500)) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];44 -> 55[label="",style="solid", color="black", weight=3];
45[label="intToDigit2 (Pos Zero) (not (primCmpInt (Pos Zero) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];45 -> 56[label="",style="solid", color="black", weight=3];
53[label="intToDigit1 (Neg (Succ vx11)) (compare (Neg (Succ vx11)) (Pos (Succ vx12)) /= LT && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];53 -> 57[label="",style="solid", color="black", weight=3];
54[label="intToDigit2 (Neg Zero) (not (primCmpInt (Neg Zero) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];54 -> 58[label="",style="solid", color="black", weight=3];
55[label="intToDigit2 (Pos (Succ vx500)) (not (primCmpInt (Pos (Succ vx500)) (Pos (Succ vx6)) == GT))",fontsize=16,color="black",shape="box"];55 -> 59[label="",style="solid", color="black", weight=3];
56[label="intToDigit2 (Pos Zero) (not (primCmpNat Zero (Succ vx6) == GT))",fontsize=16,color="black",shape="box"];56 -> 60[label="",style="solid", color="black", weight=3];
57[label="intToDigit1 (Neg (Succ vx11)) (not (compare (Neg (Succ vx11)) (Pos (Succ vx12)) == LT) && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];57 -> 61[label="",style="solid", color="black", weight=3];
58[label="intToDigit2 (Neg Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];58 -> 62[label="",style="solid", color="black", weight=3];
59 -> 306[label="",style="dashed", color="red", weight=0];
59[label="intToDigit2 (Pos (Succ vx500)) (not (primCmpNat (Succ vx500) (Succ vx6) == GT))",fontsize=16,color="magenta"];59 -> 307[label="",style="dashed", color="magenta", weight=3];
59 -> 308[label="",style="dashed", color="magenta", weight=3];
59 -> 309[label="",style="dashed", color="magenta", weight=3];
60[label="intToDigit2 (Pos Zero) (not (LT == GT))",fontsize=16,color="black",shape="box"];60 -> 64[label="",style="solid", color="black", weight=3];
61[label="intToDigit1 (Neg (Succ vx11)) (not (primCmpInt (Neg (Succ vx11)) (Pos (Succ vx12)) == LT) && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];61 -> 65[label="",style="solid", color="black", weight=3];
62[label="intToDigit2 (Neg Zero) (not False)",fontsize=16,color="black",shape="box"];62 -> 66[label="",style="solid", color="black", weight=3];
307[label="Succ vx6",fontsize=16,color="green",shape="box"];308[label="vx500",fontsize=16,color="green",shape="box"];309[label="Succ vx500",fontsize=16,color="green",shape="box"];306[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat vx41 vx42 == GT))",fontsize=16,color="burlywood",shape="triangle"];1071[label="vx41/Succ vx410",fontsize=10,color="white",style="solid",shape="box"];306 -> 1071[label="",style="solid", color="burlywood", weight=9];
1071 -> 328[label="",style="solid", color="burlywood", weight=3];
1072[label="vx41/Zero",fontsize=10,color="white",style="solid",shape="box"];306 -> 1072[label="",style="solid", color="burlywood", weight=9];
1072 -> 329[label="",style="solid", color="burlywood", weight=3];
64[label="intToDigit2 (Pos Zero) (not False)",fontsize=16,color="black",shape="box"];64 -> 69[label="",style="solid", color="black", weight=3];
65[label="intToDigit1 (Neg (Succ vx11)) (not (LT == LT) && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];65 -> 70[label="",style="solid", color="black", weight=3];
66[label="intToDigit2 (Neg Zero) True",fontsize=16,color="black",shape="box"];66 -> 71[label="",style="solid", color="black", weight=3];
328[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat (Succ vx410) vx42 == GT))",fontsize=16,color="burlywood",shape="box"];1073[label="vx42/Succ vx420",fontsize=10,color="white",style="solid",shape="box"];328 -> 1073[label="",style="solid", color="burlywood", weight=9];
1073 -> 330[label="",style="solid", color="burlywood", weight=3];
1074[label="vx42/Zero",fontsize=10,color="white",style="solid",shape="box"];328 -> 1074[label="",style="solid", color="burlywood", weight=9];
1074 -> 331[label="",style="solid", color="burlywood", weight=3];
329[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat Zero vx42 == GT))",fontsize=16,color="burlywood",shape="box"];1075[label="vx42/Succ vx420",fontsize=10,color="white",style="solid",shape="box"];329 -> 1075[label="",style="solid", color="burlywood", weight=9];
1075 -> 332[label="",style="solid", color="burlywood", weight=3];
1076[label="vx42/Zero",fontsize=10,color="white",style="solid",shape="box"];329 -> 1076[label="",style="solid", color="burlywood", weight=9];
1076 -> 333[label="",style="solid", color="burlywood", weight=3];
69[label="intToDigit2 (Pos Zero) True",fontsize=16,color="black",shape="box"];69 -> 76[label="",style="solid", color="black", weight=3];
70[label="intToDigit1 (Neg (Succ vx11)) (not True && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];70 -> 77[label="",style="solid", color="black", weight=3];
71[label="toEnum (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Neg Zero)",fontsize=16,color="black",shape="box"];71 -> 111[label="",style="solid", color="black", weight=3];
330[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat (Succ vx410) (Succ vx420) == GT))",fontsize=16,color="black",shape="box"];330 -> 334[label="",style="solid", color="black", weight=3];
331[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat (Succ vx410) Zero == GT))",fontsize=16,color="black",shape="box"];331 -> 335[label="",style="solid", color="black", weight=3];
332[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat Zero (Succ vx420) == GT))",fontsize=16,color="black",shape="box"];332 -> 336[label="",style="solid", color="black", weight=3];
333[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];333 -> 337[label="",style="solid", color="black", weight=3];
76[label="toEnum (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Pos Zero)",fontsize=16,color="black",shape="box"];76 -> 127[label="",style="solid", color="black", weight=3];
77[label="intToDigit1 (Neg (Succ vx11)) (False && Neg (Succ vx11) <= Pos (Succ vx13))",fontsize=16,color="black",shape="box"];77 -> 86[label="",style="solid", color="black", weight=3];
111 -> 138[label="",style="dashed", color="red", weight=0];
111[label="primIntToChar (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Neg Zero)",fontsize=16,color="magenta"];111 -> 139[label="",style="dashed", color="magenta", weight=3];
334 -> 306[label="",style="dashed", color="red", weight=0];
334[label="intToDigit2 (Pos (Succ vx40)) (not (primCmpNat vx410 vx420 == GT))",fontsize=16,color="magenta"];334 -> 338[label="",style="dashed", color="magenta", weight=3];
334 -> 339[label="",style="dashed", color="magenta", weight=3];
335[label="intToDigit2 (Pos (Succ vx40)) (not (GT == GT))",fontsize=16,color="black",shape="box"];335 -> 340[label="",style="solid", color="black", weight=3];
336[label="intToDigit2 (Pos (Succ vx40)) (not (LT == GT))",fontsize=16,color="black",shape="box"];336 -> 341[label="",style="solid", color="black", weight=3];
337[label="intToDigit2 (Pos (Succ vx40)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];337 -> 342[label="",style="solid", color="black", weight=3];
127 -> 140[label="",style="dashed", color="red", weight=0];
127[label="primIntToChar (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Pos Zero)",fontsize=16,color="magenta"];127 -> 141[label="",style="dashed", color="magenta", weight=3];
86[label="intToDigit1 (Neg (Succ vx11)) False",fontsize=16,color="black",shape="box"];86 -> 110[label="",style="solid", color="black", weight=3];
139[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];138[label="primIntToChar (fromEnum (Char (Succ vx19)) + Neg Zero)",fontsize=16,color="black",shape="triangle"];138 -> 142[label="",style="solid", color="black", weight=3];
338[label="vx420",fontsize=16,color="green",shape="box"];339[label="vx410",fontsize=16,color="green",shape="box"];340[label="intToDigit2 (Pos (Succ vx40)) (not True)",fontsize=16,color="black",shape="box"];340 -> 343[label="",style="solid", color="black", weight=3];
341[label="intToDigit2 (Pos (Succ vx40)) (not False)",fontsize=16,color="black",shape="triangle"];341 -> 344[label="",style="solid", color="black", weight=3];
342 -> 341[label="",style="dashed", color="red", weight=0];
342[label="intToDigit2 (Pos (Succ vx40)) (not False)",fontsize=16,color="magenta"];141[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];140[label="primIntToChar (fromEnum (Char (Succ vx21)) + Pos Zero)",fontsize=16,color="black",shape="triangle"];140 -> 143[label="",style="solid", color="black", weight=3];
110[label="intToDigit0 (Neg (Succ vx11)) otherwise",fontsize=16,color="black",shape="box"];110 -> 137[label="",style="solid", color="black", weight=3];
142[label="primIntToChar (primPlusInt (fromEnum (Char (Succ vx19))) (Neg Zero))",fontsize=16,color="black",shape="box"];142 -> 151[label="",style="solid", color="black", weight=3];
343[label="intToDigit2 (Pos (Succ vx40)) False",fontsize=16,color="black",shape="box"];343 -> 345[label="",style="solid", color="black", weight=3];
344[label="intToDigit2 (Pos (Succ vx40)) True",fontsize=16,color="black",shape="box"];344 -> 346[label="",style="solid", color="black", weight=3];
143[label="primIntToChar (primPlusInt (fromEnum (Char (Succ vx21))) (Pos Zero))",fontsize=16,color="black",shape="box"];143 -> 152[label="",style="solid", color="black", weight=3];
137[label="intToDigit0 (Neg (Succ vx11)) True",fontsize=16,color="black",shape="box"];137 -> 150[label="",style="solid", color="black", weight=3];
151[label="primIntToChar (primPlusInt (primCharToInt (Char (Succ vx19))) (Neg Zero))",fontsize=16,color="black",shape="box"];151 -> 161[label="",style="solid", color="black", weight=3];
345 -> 353[label="",style="dashed", color="red", weight=0];
345[label="intToDigit1 (Pos (Succ vx40)) (Pos (Succ vx40) >= Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))) && Pos (Succ vx40) <= Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))",fontsize=16,color="magenta"];345 -> 354[label="",style="dashed", color="magenta", weight=3];
345 -> 355[label="",style="dashed", color="magenta", weight=3];
345 -> 356[label="",style="dashed", color="magenta", weight=3];
346[label="toEnum (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ vx40))",fontsize=16,color="black",shape="box"];346 -> 371[label="",style="solid", color="black", weight=3];
152[label="primIntToChar (primPlusInt (primCharToInt (Char (Succ vx21))) (Pos Zero))",fontsize=16,color="black",shape="box"];152 -> 164[label="",style="solid", color="black", weight=3];
150[label="error []",fontsize=16,color="black",shape="triangle"];150 -> 165[label="",style="solid", color="black", weight=3];
161[label="primIntToChar (primPlusInt (Pos (Succ vx19)) (Neg Zero))",fontsize=16,color="black",shape="box"];161 -> 166[label="",style="solid", color="black", weight=3];
354[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))",fontsize=16,color="green",shape="box"];355[label="vx40",fontsize=16,color="green",shape="box"];356[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))",fontsize=16,color="green",shape="box"];353[label="intToDigit1 (Pos (Succ vx50)) (Pos (Succ vx50) >= Pos (Succ vx51) && Pos (Succ vx50) <= Pos (Succ vx52))",fontsize=16,color="black",shape="triangle"];353 -> 360[label="",style="solid", color="black", weight=3];
371 -> 382[label="",style="dashed", color="red", weight=0];
371[label="primIntToChar (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ vx40))",fontsize=16,color="magenta"];371 -> 383[label="",style="dashed", color="magenta", weight=3];
371 -> 384[label="",style="dashed", color="magenta", weight=3];
164[label="primIntToChar (primPlusInt (Pos (Succ vx21)) (Pos Zero))",fontsize=16,color="black",shape="box"];164 -> 189[label="",style="solid", color="black", weight=3];
165[label="error []",fontsize=16,color="red",shape="box"];166[label="primIntToChar (primMinusNat (Succ vx19) Zero)",fontsize=16,color="black",shape="box"];166 -> 190[label="",style="solid", color="black", weight=3];
360[label="intToDigit1 (Pos (Succ vx50)) (compare (Pos (Succ vx50)) (Pos (Succ vx51)) /= LT && Pos (Succ vx50) <= Pos (Succ vx52))",fontsize=16,color="black",shape="box"];360 -> 370[label="",style="solid", color="black", weight=3];
383[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];384[label="vx40",fontsize=16,color="green",shape="box"];382[label="primIntToChar (fromEnum (Char (Succ vx54)) + Pos (Succ vx55))",fontsize=16,color="black",shape="triangle"];382 -> 385[label="",style="solid", color="black", weight=3];
189[label="primIntToChar (Pos (primPlusNat (Succ vx21) Zero))",fontsize=16,color="black",shape="box"];189 -> 207[label="",style="solid", color="black", weight=3];
190[label="primIntToChar (Pos (Succ vx19))",fontsize=16,color="black",shape="triangle"];190 -> 208[label="",style="solid", color="black", weight=3];
370[label="intToDigit1 (Pos (Succ vx50)) (not (compare (Pos (Succ vx50)) (Pos (Succ vx51)) == LT) && Pos (Succ vx50) <= Pos (Succ vx52))",fontsize=16,color="black",shape="box"];370 -> 381[label="",style="solid", color="black", weight=3];
385[label="primIntToChar (primPlusInt (fromEnum (Char (Succ vx54))) (Pos (Succ vx55)))",fontsize=16,color="black",shape="box"];385 -> 387[label="",style="solid", color="black", weight=3];
207[label="Char (primPlusNat (Succ vx21) Zero)",fontsize=16,color="green",shape="box"];207 -> 220[label="",style="dashed", color="green", weight=3];
208[label="Char (Succ vx19)",fontsize=16,color="green",shape="box"];381[label="intToDigit1 (Pos (Succ vx50)) (not (primCmpInt (Pos (Succ vx50)) (Pos (Succ vx51)) == LT) && Pos (Succ vx50) <= Pos (Succ vx52))",fontsize=16,color="black",shape="box"];381 -> 386[label="",style="solid", color="black", weight=3];
387[label="primIntToChar (primPlusInt (primCharToInt (Char (Succ vx54))) (Pos (Succ vx55)))",fontsize=16,color="black",shape="box"];387 -> 389[label="",style="solid", color="black", weight=3];
220[label="primPlusNat (Succ vx21) Zero",fontsize=16,color="black",shape="box"];220 -> 237[label="",style="solid", color="black", weight=3];
386 -> 523[label="",style="dashed", color="red", weight=0];
386[label="intToDigit1 (Pos (Succ vx50)) (not (primCmpNat (Succ vx50) (Succ vx51) == LT) && Pos (Succ vx50) <= Pos (Succ vx52))",fontsize=16,color="magenta"];386 -> 524[label="",style="dashed", color="magenta", weight=3];
386 -> 525[label="",style="dashed", color="magenta", weight=3];
386 -> 526[label="",style="dashed", color="magenta", weight=3];
386 -> 527[label="",style="dashed", color="magenta", weight=3];
389[label="primIntToChar (primPlusInt (Pos (Succ vx54)) (Pos (Succ vx55)))",fontsize=16,color="black",shape="box"];389 -> 392[label="",style="solid", color="black", weight=3];
237[label="Succ vx21",fontsize=16,color="green",shape="box"];524[label="vx50",fontsize=16,color="green",shape="box"];525[label="vx52",fontsize=16,color="green",shape="box"];526[label="Succ vx51",fontsize=16,color="green",shape="box"];527[label="Succ vx50",fontsize=16,color="green",shape="box"];523[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat vx58 vx59 == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="burlywood",shape="triangle"];1084[label="vx58/Succ vx580",fontsize=10,color="white",style="solid",shape="box"];523 -> 1084[label="",style="solid", color="burlywood", weight=9];
1084 -> 552[label="",style="solid", color="burlywood", weight=3];
1085[label="vx58/Zero",fontsize=10,color="white",style="solid",shape="box"];523 -> 1085[label="",style="solid", color="burlywood", weight=9];
1085 -> 553[label="",style="solid", color="burlywood", weight=3];
392[label="primIntToChar (Pos (primPlusNat (Succ vx54) (Succ vx55)))",fontsize=16,color="black",shape="box"];392 -> 397[label="",style="solid", color="black", weight=3];
552[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat (Succ vx580) vx59 == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="burlywood",shape="box"];1086[label="vx59/Succ vx590",fontsize=10,color="white",style="solid",shape="box"];552 -> 1086[label="",style="solid", color="burlywood", weight=9];
1086 -> 554[label="",style="solid", color="burlywood", weight=3];
1087[label="vx59/Zero",fontsize=10,color="white",style="solid",shape="box"];552 -> 1087[label="",style="solid", color="burlywood", weight=9];
1087 -> 555[label="",style="solid", color="burlywood", weight=3];
553[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat Zero vx59 == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="burlywood",shape="box"];1088[label="vx59/Succ vx590",fontsize=10,color="white",style="solid",shape="box"];553 -> 1088[label="",style="solid", color="burlywood", weight=9];
1088 -> 556[label="",style="solid", color="burlywood", weight=3];
1089[label="vx59/Zero",fontsize=10,color="white",style="solid",shape="box"];553 -> 1089[label="",style="solid", color="burlywood", weight=9];
1089 -> 557[label="",style="solid", color="burlywood", weight=3];
397[label="Char (primPlusNat (Succ vx54) (Succ vx55))",fontsize=16,color="green",shape="box"];397 -> 402[label="",style="dashed", color="green", weight=3];
554[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat (Succ vx580) (Succ vx590) == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];554 -> 558[label="",style="solid", color="black", weight=3];
555[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat (Succ vx580) Zero == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];555 -> 559[label="",style="solid", color="black", weight=3];
556[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat Zero (Succ vx590) == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];556 -> 560[label="",style="solid", color="black", weight=3];
557[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat Zero Zero == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];557 -> 561[label="",style="solid", color="black", weight=3];
402[label="primPlusNat (Succ vx54) (Succ vx55)",fontsize=16,color="black",shape="box"];402 -> 408[label="",style="solid", color="black", weight=3];
558 -> 523[label="",style="dashed", color="red", weight=0];
558[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat vx580 vx590 == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="magenta"];558 -> 562[label="",style="dashed", color="magenta", weight=3];
558 -> 563[label="",style="dashed", color="magenta", weight=3];
559[label="intToDigit1 (Pos (Succ vx57)) (not (GT == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];559 -> 564[label="",style="solid", color="black", weight=3];
560[label="intToDigit1 (Pos (Succ vx57)) (not (LT == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];560 -> 565[label="",style="solid", color="black", weight=3];
561[label="intToDigit1 (Pos (Succ vx57)) (not (EQ == LT) && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];561 -> 566[label="",style="solid", color="black", weight=3];
408[label="Succ (Succ (primPlusNat vx54 vx55))",fontsize=16,color="green",shape="box"];408 -> 416[label="",style="dashed", color="green", weight=3];
562[label="vx590",fontsize=16,color="green",shape="box"];563[label="vx580",fontsize=16,color="green",shape="box"];564[label="intToDigit1 (Pos (Succ vx57)) (not False && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="triangle"];564 -> 567[label="",style="solid", color="black", weight=3];
565[label="intToDigit1 (Pos (Succ vx57)) (not True && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];565 -> 568[label="",style="solid", color="black", weight=3];
566 -> 564[label="",style="dashed", color="red", weight=0];
566[label="intToDigit1 (Pos (Succ vx57)) (not False && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="magenta"];416[label="primPlusNat vx54 vx55",fontsize=16,color="burlywood",shape="triangle"];1092[label="vx54/Succ vx540",fontsize=10,color="white",style="solid",shape="box"];416 -> 1092[label="",style="solid", color="burlywood", weight=9];
1092 -> 424[label="",style="solid", color="burlywood", weight=3];
1093[label="vx54/Zero",fontsize=10,color="white",style="solid",shape="box"];416 -> 1093[label="",style="solid", color="burlywood", weight=9];
1093 -> 425[label="",style="solid", color="burlywood", weight=3];
567[label="intToDigit1 (Pos (Succ vx57)) (True && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];567 -> 569[label="",style="solid", color="black", weight=3];
568[label="intToDigit1 (Pos (Succ vx57)) (False && Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];568 -> 570[label="",style="solid", color="black", weight=3];
424[label="primPlusNat (Succ vx540) vx55",fontsize=16,color="burlywood",shape="box"];1094[label="vx55/Succ vx550",fontsize=10,color="white",style="solid",shape="box"];424 -> 1094[label="",style="solid", color="burlywood", weight=9];
1094 -> 434[label="",style="solid", color="burlywood", weight=3];
1095[label="vx55/Zero",fontsize=10,color="white",style="solid",shape="box"];424 -> 1095[label="",style="solid", color="burlywood", weight=9];
1095 -> 435[label="",style="solid", color="burlywood", weight=3];
425[label="primPlusNat Zero vx55",fontsize=16,color="burlywood",shape="box"];1096[label="vx55/Succ vx550",fontsize=10,color="white",style="solid",shape="box"];425 -> 1096[label="",style="solid", color="burlywood", weight=9];
1096 -> 436[label="",style="solid", color="burlywood", weight=3];
1097[label="vx55/Zero",fontsize=10,color="white",style="solid",shape="box"];425 -> 1097[label="",style="solid", color="burlywood", weight=9];
1097 -> 437[label="",style="solid", color="burlywood", weight=3];
569[label="intToDigit1 (Pos (Succ vx57)) (Pos (Succ vx57) <= Pos (Succ vx60))",fontsize=16,color="black",shape="box"];569 -> 571[label="",style="solid", color="black", weight=3];
570[label="intToDigit1 (Pos (Succ vx57)) False",fontsize=16,color="black",shape="triangle"];570 -> 572[label="",style="solid", color="black", weight=3];
434[label="primPlusNat (Succ vx540) (Succ vx550)",fontsize=16,color="black",shape="box"];434 -> 447[label="",style="solid", color="black", weight=3];
435[label="primPlusNat (Succ vx540) Zero",fontsize=16,color="black",shape="box"];435 -> 448[label="",style="solid", color="black", weight=3];
436[label="primPlusNat Zero (Succ vx550)",fontsize=16,color="black",shape="box"];436 -> 449[label="",style="solid", color="black", weight=3];
437[label="primPlusNat Zero Zero",fontsize=16,color="black",shape="box"];437 -> 450[label="",style="solid", color="black", weight=3];
571[label="intToDigit1 (Pos (Succ vx57)) (compare (Pos (Succ vx57)) (Pos (Succ vx60)) /= GT)",fontsize=16,color="black",shape="box"];571 -> 573[label="",style="solid", color="black", weight=3];
572[label="intToDigit0 (Pos (Succ vx57)) otherwise",fontsize=16,color="black",shape="box"];572 -> 574[label="",style="solid", color="black", weight=3];
447[label="Succ (Succ (primPlusNat vx540 vx550))",fontsize=16,color="green",shape="box"];447 -> 459[label="",style="dashed", color="green", weight=3];
448[label="Succ vx540",fontsize=16,color="green",shape="box"];449[label="Succ vx550",fontsize=16,color="green",shape="box"];450[label="Zero",fontsize=16,color="green",shape="box"];573[label="intToDigit1 (Pos (Succ vx57)) (not (compare (Pos (Succ vx57)) (Pos (Succ vx60)) == GT))",fontsize=16,color="black",shape="box"];573 -> 575[label="",style="solid", color="black", weight=3];
574[label="intToDigit0 (Pos (Succ vx57)) True",fontsize=16,color="black",shape="box"];574 -> 576[label="",style="solid", color="black", weight=3];
459 -> 416[label="",style="dashed", color="red", weight=0];
459[label="primPlusNat vx540 vx550",fontsize=16,color="magenta"];459 -> 468[label="",style="dashed", color="magenta", weight=3];
459 -> 469[label="",style="dashed", color="magenta", weight=3];
575[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpInt (Pos (Succ vx57)) (Pos (Succ vx60)) == GT))",fontsize=16,color="black",shape="box"];575 -> 577[label="",style="solid", color="black", weight=3];
576 -> 150[label="",style="dashed", color="red", weight=0];
576[label="error []",fontsize=16,color="magenta"];468[label="vx540",fontsize=16,color="green",shape="box"];469[label="vx550",fontsize=16,color="green",shape="box"];577 -> 907[label="",style="dashed", color="red", weight=0];
577[label="intToDigit1 (Pos (Succ vx57)) (not (primCmpNat (Succ vx57) (Succ vx60) == GT))",fontsize=16,color="magenta"];577 -> 908[label="",style="dashed", color="magenta", weight=3];
577 -> 909[label="",style="dashed", color="magenta", weight=3];
577 -> 910[label="",style="dashed", color="magenta", weight=3];
908[label="Succ vx57",fontsize=16,color="green",shape="box"];909[label="Succ vx60",fontsize=16,color="green",shape="box"];910[label="vx57",fontsize=16,color="green",shape="box"];907[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat vx115 vx116 == GT))",fontsize=16,color="burlywood",shape="triangle"];1101[label="vx115/Succ vx1150",fontsize=10,color="white",style="solid",shape="box"];907 -> 1101[label="",style="solid", color="burlywood", weight=9];
1101 -> 938[label="",style="solid", color="burlywood", weight=3];
1102[label="vx115/Zero",fontsize=10,color="white",style="solid",shape="box"];907 -> 1102[label="",style="solid", color="burlywood", weight=9];
1102 -> 939[label="",style="solid", color="burlywood", weight=3];
938[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat (Succ vx1150) vx116 == GT))",fontsize=16,color="burlywood",shape="box"];1103[label="vx116/Succ vx1160",fontsize=10,color="white",style="solid",shape="box"];938 -> 1103[label="",style="solid", color="burlywood", weight=9];
1103 -> 940[label="",style="solid", color="burlywood", weight=3];
1104[label="vx116/Zero",fontsize=10,color="white",style="solid",shape="box"];938 -> 1104[label="",style="solid", color="burlywood", weight=9];
1104 -> 941[label="",style="solid", color="burlywood", weight=3];
939[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat Zero vx116 == GT))",fontsize=16,color="burlywood",shape="box"];1105[label="vx116/Succ vx1160",fontsize=10,color="white",style="solid",shape="box"];939 -> 1105[label="",style="solid", color="burlywood", weight=9];
1105 -> 942[label="",style="solid", color="burlywood", weight=3];
1106[label="vx116/Zero",fontsize=10,color="white",style="solid",shape="box"];939 -> 1106[label="",style="solid", color="burlywood", weight=9];
1106 -> 943[label="",style="solid", color="burlywood", weight=3];
940[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat (Succ vx1150) (Succ vx1160) == GT))",fontsize=16,color="black",shape="box"];940 -> 944[label="",style="solid", color="black", weight=3];
941[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat (Succ vx1150) Zero == GT))",fontsize=16,color="black",shape="box"];941 -> 945[label="",style="solid", color="black", weight=3];
942[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat Zero (Succ vx1160) == GT))",fontsize=16,color="black",shape="box"];942 -> 946[label="",style="solid", color="black", weight=3];
943[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat Zero Zero == GT))",fontsize=16,color="black",shape="box"];943 -> 947[label="",style="solid", color="black", weight=3];
944 -> 907[label="",style="dashed", color="red", weight=0];
944[label="intToDigit1 (Pos (Succ vx114)) (not (primCmpNat vx1150 vx1160 == GT))",fontsize=16,color="magenta"];944 -> 948[label="",style="dashed", color="magenta", weight=3];
944 -> 949[label="",style="dashed", color="magenta", weight=3];
945[label="intToDigit1 (Pos (Succ vx114)) (not (GT == GT))",fontsize=16,color="black",shape="box"];945 -> 950[label="",style="solid", color="black", weight=3];
946[label="intToDigit1 (Pos (Succ vx114)) (not (LT == GT))",fontsize=16,color="black",shape="box"];946 -> 951[label="",style="solid", color="black", weight=3];
947[label="intToDigit1 (Pos (Succ vx114)) (not (EQ == GT))",fontsize=16,color="black",shape="box"];947 -> 952[label="",style="solid", color="black", weight=3];
948[label="vx1150",fontsize=16,color="green",shape="box"];949[label="vx1160",fontsize=16,color="green",shape="box"];950[label="intToDigit1 (Pos (Succ vx114)) (not True)",fontsize=16,color="black",shape="box"];950 -> 953[label="",style="solid", color="black", weight=3];
951[label="intToDigit1 (Pos (Succ vx114)) (not False)",fontsize=16,color="black",shape="triangle"];951 -> 954[label="",style="solid", color="black", weight=3];
952 -> 951[label="",style="dashed", color="red", weight=0];
952[label="intToDigit1 (Pos (Succ vx114)) (not False)",fontsize=16,color="magenta"];953 -> 570[label="",style="dashed", color="red", weight=0];
953[label="intToDigit1 (Pos (Succ vx114)) False",fontsize=16,color="magenta"];953 -> 955[label="",style="dashed", color="magenta", weight=3];
954[label="intToDigit1 (Pos (Succ vx114)) True",fontsize=16,color="black",shape="box"];954 -> 956[label="",style="solid", color="black", weight=3];
955[label="vx114",fontsize=16,color="green",shape="box"];956[label="toEnum (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ vx114) - Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))",fontsize=16,color="black",shape="box"];956 -> 985[label="",style="solid", color="black", weight=3];
985 -> 1025[label="",style="dashed", color="red", weight=0];
985[label="primIntToChar (fromEnum (Char (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + Pos (Succ vx114) - Pos (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))",fontsize=16,color="magenta"];985 -> 1026[label="",style="dashed", color="magenta", weight=3];
985 -> 1027[label="",style="dashed", color="magenta", weight=3];
985 -> 1028[label="",style="dashed", color="magenta", weight=3];
1026[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))",fontsize=16,color="green",shape="box"];1027[label="vx114",fontsize=16,color="green",shape="box"];1028[label="Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))))))))",fontsize=16,color="green",shape="box"];1025[label="primIntToChar (fromEnum (Char (Succ vx128)) + Pos (Succ vx129) - Pos (Succ vx130))",fontsize=16,color="black",shape="triangle"];1025 -> 1032[label="",style="solid", color="black", weight=3];
1032[label="primIntToChar (primMinusInt (fromEnum (Char (Succ vx128)) + Pos (Succ vx129)) (Pos (Succ vx130)))",fontsize=16,color="black",shape="box"];1032 -> 1033[label="",style="solid", color="black", weight=3];
1033[label="primIntToChar (primMinusInt (primPlusInt (fromEnum (Char (Succ vx128))) (Pos (Succ vx129))) (Pos (Succ vx130)))",fontsize=16,color="black",shape="box"];1033 -> 1034[label="",style="solid", color="black", weight=3];
1034[label="primIntToChar (primMinusInt (primPlusInt (primCharToInt (Char (Succ vx128))) (Pos (Succ vx129))) (Pos (Succ vx130)))",fontsize=16,color="black",shape="box"];1034 -> 1035[label="",style="solid", color="black", weight=3];
1035[label="primIntToChar (primMinusInt (primPlusInt (Pos (Succ vx128)) (Pos (Succ vx129))) (Pos (Succ vx130)))",fontsize=16,color="black",shape="box"];1035 -> 1036[label="",style="solid", color="black", weight=3];
1036 -> 1037[label="",style="dashed", color="red", weight=0];
1036[label="primIntToChar (primMinusInt (Pos (primPlusNat (Succ vx128) (Succ vx129))) (Pos (Succ vx130)))",fontsize=16,color="magenta"];1036 -> 1038[label="",style="dashed", color="magenta", weight=3];
1038 -> 416[label="",style="dashed", color="red", weight=0];
1038[label="primPlusNat (Succ vx128) (Succ vx129)",fontsize=16,color="magenta"];1038 -> 1039[label="",style="dashed", color="magenta", weight=3];
1038 -> 1040[label="",style="dashed", color="magenta", weight=3];
1037[label="primIntToChar (primMinusInt (Pos vx131) (Pos (Succ vx130)))",fontsize=16,color="black",shape="triangle"];1037 -> 1041[label="",style="solid", color="black", weight=3];
1039[label="Succ vx128",fontsize=16,color="green",shape="box"];1040[label="Succ vx129",fontsize=16,color="green",shape="box"];1041[label="primIntToChar (primMinusNat vx131 (Succ vx130))",fontsize=16,color="burlywood",shape="box"];1113[label="vx131/Succ vx1310",fontsize=10,color="white",style="solid",shape="box"];1041 -> 1113[label="",style="solid", color="burlywood", weight=9];
1113 -> 1042[label="",style="solid", color="burlywood", weight=3];
1114[label="vx131/Zero",fontsize=10,color="white",style="solid",shape="box"];1041 -> 1114[label="",style="solid", color="burlywood", weight=9];
1114 -> 1043[label="",style="solid", color="burlywood", weight=3];
1042[label="primIntToChar (primMinusNat (Succ vx1310) (Succ vx130))",fontsize=16,color="black",shape="box"];1042 -> 1044[label="",style="solid", color="black", weight=3];
1043[label="primIntToChar (primMinusNat Zero (Succ vx130))",fontsize=16,color="black",shape="box"];1043 -> 1045[label="",style="solid", color="black", weight=3];
1044[label="primIntToChar (primMinusNat vx1310 vx130)",fontsize=16,color="burlywood",shape="triangle"];1115[label="vx1310/Succ vx13100",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1115[label="",style="solid", color="burlywood", weight=9];
1115 -> 1046[label="",style="solid", color="burlywood", weight=3];
1116[label="vx1310/Zero",fontsize=10,color="white",style="solid",shape="box"];1044 -> 1116[label="",style="solid", color="burlywood", weight=9];
1116 -> 1047[label="",style="solid", color="burlywood", weight=3];
1045[label="primIntToChar (Neg (Succ vx130))",fontsize=16,color="black",shape="triangle"];1045 -> 1048[label="",style="solid", color="black", weight=3];
1046[label="primIntToChar (primMinusNat (Succ vx13100) vx130)",fontsize=16,color="burlywood",shape="box"];1117[label="vx130/Succ vx1300",fontsize=10,color="white",style="solid",shape="box"];1046 -> 1117[label="",style="solid", color="burlywood", weight=9];
1117 -> 1049[label="",style="solid", color="burlywood", weight=3];
1118[label="vx130/Zero",fontsize=10,color="white",style="solid",shape="box"];1046 -> 1118[label="",style="solid", color="burlywood", weight=9];
1118 -> 1050[label="",style="solid", color="burlywood", weight=3];
1047[label="primIntToChar (primMinusNat Zero vx130)",fontsize=16,color="burlywood",shape="box"];1119[label="vx130/Succ vx1300",fontsize=10,color="white",style="solid",shape="box"];1047 -> 1119[label="",style="solid", color="burlywood", weight=9];
1119 -> 1051[label="",style="solid", color="burlywood", weight=3];
1120[label="vx130/Zero",fontsize=10,color="white",style="solid",shape="box"];1047 -> 1120[label="",style="solid", color="burlywood", weight=9];
1120 -> 1052[label="",style="solid", color="burlywood", weight=3];
1048[label="error []",fontsize=16,color="red",shape="box"];1049[label="primIntToChar (primMinusNat (Succ vx13100) (Succ vx1300))",fontsize=16,color="black",shape="box"];1049 -> 1053[label="",style="solid", color="black", weight=3];
1050[label="primIntToChar (primMinusNat (Succ vx13100) Zero)",fontsize=16,color="black",shape="box"];1050 -> 1054[label="",style="solid", color="black", weight=3];
1051[label="primIntToChar (primMinusNat Zero (Succ vx1300))",fontsize=16,color="black",shape="box"];1051 -> 1055[label="",style="solid", color="black", weight=3];
1052[label="primIntToChar (primMinusNat Zero Zero)",fontsize=16,color="black",shape="box"];1052 -> 1056[label="",style="solid", color="black", weight=3];
1053 -> 1044[label="",style="dashed", color="red", weight=0];
1053[label="primIntToChar (primMinusNat vx13100 vx1300)",fontsize=16,color="magenta"];1053 -> 1057[label="",style="dashed", color="magenta", weight=3];
1053 -> 1058[label="",style="dashed", color="magenta", weight=3];
1054 -> 190[label="",style="dashed", color="red", weight=0];
1054[label="primIntToChar (Pos (Succ vx13100))",fontsize=16,color="magenta"];1054 -> 1059[label="",style="dashed", color="magenta", weight=3];
1055 -> 1045[label="",style="dashed", color="red", weight=0];
1055[label="primIntToChar (Neg (Succ vx1300))",fontsize=16,color="magenta"];1055 -> 1060[label="",style="dashed", color="magenta", weight=3];
1056[label="primIntToChar (Pos Zero)",fontsize=16,color="black",shape="box"];1056 -> 1061[label="",style="solid", color="black", weight=3];
1057[label="vx1300",fontsize=16,color="green",shape="box"];1058[label="vx13100",fontsize=16,color="green",shape="box"];1059[label="vx13100",fontsize=16,color="green",shape="box"];1060[label="vx1300",fontsize=16,color="green",shape="box"];1061[label="Char Zero",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(vx540), Succ(vx550)) → new_primPlusNat(vx540, vx550)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_primPlusNat(Succ(vx540), Succ(vx550)) → new_primPlusNat(vx540, vx550)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primIntToChar(Succ(vx13100), Succ(vx1300)) → new_primIntToChar(vx13100, vx1300)

From the DPs we obtained the following set of size-change graphs:

new_primIntToChar(Succ(vx13100), Succ(vx1300)) → new_primIntToChar(vx13100, vx1300)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_intToDigit1(vx114, Succ(vx1150), Succ(vx1160)) → new_intToDigit1(vx114, vx1150, vx1160)

From the DPs we obtained the following set of size-change graphs:

new_intToDigit1(vx114, Succ(vx1150), Succ(vx1160)) → new_intToDigit1(vx114, vx1150, vx1160)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_intToDigit10(vx57, Succ(vx580), Succ(vx590), vx60) → new_intToDigit10(vx57, vx580, vx590, vx60)

From the DPs we obtained the following set of size-change graphs:

new_intToDigit10(vx57, Succ(vx580), Succ(vx590), vx60) → new_intToDigit10(vx57, vx580, vx590, vx60)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3, 4 >= 4

↳ HASKELL

  ↳ BR

    ↳ HASKELL

      ↳ COR

        ↳ HASKELL

          ↳ NumRed

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_intToDigit2(vx40, Succ(vx410), Succ(vx420)) → new_intToDigit2(vx40, vx410, vx420)

From the DPs we obtained the following set of size-change graphs:

new_intToDigit2(vx40, Succ(vx410), Succ(vx420)) → new_intToDigit2(vx40, vx410, vx420)
The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

intToDigit1	i True	= toEnum (fromEnum 'a' + i - 10)
intToDigit1	i False	= intToDigit0 i otherwise

intToDigit2	i True	= toEnum (fromEnum '0' + i)
intToDigit2	i False	= intToDigit1 i (i >= 10 && i <= 15)